$\forall$$T$:Type, $l$:$T$ List, $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$l$$\parallel$}}$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$+1}}$, $x$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$$-$$j$}}$. l\_interval($l$;$j$;$i$)[$x$] $=$ $l$[$j$+$x$] $\in$ $T$